a, b, r, s:. r  a  s  r  b  s  qdist(a;b)  s - r 

latex

Definitions	r - s, ff, tt, if b then t else f fi , T, P  Q, P  Q, True, , t  T, |r|, P & Q, qdist(r;s), a  b  c, P  Q, x:A. B(x), Unit, , S  T,
Lemmas	qadd-non-neg, qadd com, qmul wf, qadd assoc, qadd wf, int inc rationals, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, qminus-qsub, ifthenelse wf, true wf, squash wf, not wf, bnot wf, assert wf, qle-normalize, bool wf, qsub wf, qpositive wf, rationals wf, qle wf